\begin{tabbing}
R{-}Feasible\=\{i:l\}\+
\\[0ex](Rplus(\=ecl{-}machine\=\{ecl:ut2\}\+\+
\\[0ex](\=mkid\{b:ut2\};\+
\\[0ex]fpf{-}join(\=id{-}deq;\+
\\[0ex]fpf{-}single(mkid\{x1:ut2\}; int\_seg(0; 3));
\\[0ex]fpf{-}join(\=id{-}deq;\+
\\[0ex]fpf{-}single(mkid\{v1:ut2\}; int\_seg(0; 3));
\\[0ex]fpf{-}join(\=id{-}deq;\+
\\[0ex]fpf{-}single(mkid\{win:ut2\}; $\mathbb{Z}$);
\\[0ex]fpf{-}join(\=id{-}deq;\+
\\[0ex]fpf{-}single(\=mkid\{x2:ut2\};\+
\\[0ex]int\_seg(0; 3)
\\[0ex]);
\-\\[0ex]fpf{-}single(\=mkid\{v2:ut2\};\+
\\[0ex]int\_seg(0; 3))
\-\\[0ex]))));
\-\-\-\-\\[0ex]fpf{-}join(\=Kind{-}deq;\+
\\[0ex]fpf{-}join(\=Kind{-}deq;\+
\\[0ex]fpf{-}single(\=rcv(mklnk\{\=input:ut2,\+\+
\\[0ex]b:ut2,
\\[0ex]1:ut2
\\[0ex]\},mkid\{play:ut2\});
\-\\[0ex]int\_seg(0; 3));
\-\\[0ex]fpf{-}single(\=locl(mkid\{choose1:ut2\});\+
\\[0ex]p{-}outcome(ternary{-}fps)));
\-\-\\[0ex]fpf{-}join(\=Kind{-}deq;\+
\\[0ex]fpf{-}single(\=locl(mkid\{diff:ut2\});\+
\\[0ex]int\_seg(0; 1));
\-\\[0ex]fpf{-}join(\=Kind{-}deq;\+
\\[0ex]fpf{-}single(\=locl(mkid\{same:ut2\});\+
\\[0ex]int\_seg(0; 1));
\-\\[0ex]fpf{-}single
\\[0ex](\=rcv(mklnk\{\=b:ut2,\+\+
\\[0ex]output:ut2,
\\[0ex]1:ut2
\\[0ex]\},mkid\{hello:ut2\});
\-\\[0ex]$\mathbb{B}$))));
\-\-\-\-\\[0ex]eclact(\=eclcatch\+
\\[0ex](\=eclrepeat\+
\\[0ex](eclseq(\=ecland(\=eclbase(\=rcv(mklnk\{\=input:ut2,\+\+\+\+
\\[0ex]b:ut2,
\\[0ex]1:ut2
\\[0ex]\},mkid\{play:ut2\});
\-\\[0ex]($\lambda$$s$,$v$. tt));
\-\\[0ex]eclbase(\=locl(mkid\{choose1:ut2\});\+
\\[0ex]($\lambda$$s$,$v$. tt)));
\-\-\\[0ex]eclor(\=eclthrow(\=eclbase(\=locl(mkid\{diff:ut2\});\+\+\+
\\[0ex]($\lambda$$s$,$v$. tt));
\-\\[0ex]1);
\-\\[0ex]eclbase(\=locl(mkid\{same:ut2\});\+
\\[0ex]($\lambda$$s$,$v$. tt)))));
\-\-\-\\[0ex]cons(1; []));
\-\\[0ex]1);
\-\\[0ex]msg{-}spec1(\=locl(mkid\{diff:ut2\});\+
\\[0ex]mklnk\{b:ut2, output:ut2, 1:ut2\};
\\[0ex]mkid\{hello:ut2\};
\\[0ex]1;
\\[0ex]$s$,$v$.rps(($s$(mkid\{x1:ut2\})); ($s$(mkid\{v1:ut2\}))));
\-\\[0ex]update{-}spec1(\=locl(mkid\{diff:ut2\});\+
\\[0ex]mkid\{win:ut2\};
\\[0ex]1;
\\[0ex]$s$,$v$.(($s$(mkid\{win:ut2\}))
\\[0ex]+ \=if rps(($s$(mkid\{x1:ut2\})); ($s$(mkid\{v1:ut2\})))\+
\\[0ex]then 1
\\[0ex]else 0
\\[0ex]fi )));
\-\-\-\-\\[0ex]Rplus(\=Rplus(\=Rpre(\=mkid\{b:ut2\};\+\+\+
\\[0ex]fpf{-}join(\=id{-}deq;\+
\\[0ex]fpf{-}single(mkid\{x1:ut2\}; int\_seg(0; 3));
\\[0ex]fpf{-}single(mkid\{v1:ut2\}; int\_seg(0; 3)));
\-\\[0ex]mkid\{diff:ut2\};
\\[0ex]unit{-}fps;
\\[0ex]($\lambda$$s$.$\neg_{b}$($s$(mkid\{x1:ut2\}) =$_{0}$ $s$(mkid\{v1:ut2\}))));
\-\\[0ex]Rpre(\=mkid\{b:ut2\};\+
\\[0ex]fpf{-}join(\=id{-}deq;\+
\\[0ex]fpf{-}single(mkid\{x1:ut2\}; int\_seg(0; 3));
\\[0ex]fpf{-}single(mkid\{v1:ut2\}; int\_seg(0; 3)));
\-\\[0ex]mkid\{same:ut2\};
\\[0ex]unit{-}fps;
\\[0ex]($\lambda$$s$.($s$(mkid\{x1:ut2\}) =$_{0}$ $s$(mkid\{v1:ut2\})))));
\-\-\\[0ex]Rplus(\=Rpre(\=mkid\{b:ut2\};\+\+
\\[0ex]fpf{-}empty;
\\[0ex]mkid\{choose1:ut2\};
\\[0ex]ternary{-}fps;
\\[0ex]($\lambda$$s$.tt));
\-\\[0ex]Rplus(\=Reffect(\=mkid\{b:ut2\};\+\+
\\[0ex]fpf{-}single(mkid\{x1:ut2\}; int\_seg(0; 3));
\\[0ex]rcv(mklnk\{\=input:ut2, b:ut2, 1:ut2\+
\\[0ex]\},mkid\{play:ut2\});
\-\\[0ex]int\_seg(0; 3);
\\[0ex]mkid\{x1:ut2\};
\\[0ex](inl ($\lambda$$s$,$v$. $v$) ));
\-\\[0ex]Reffect(\=mkid\{b:ut2\};\+
\\[0ex]fpf{-}single(mkid\{v1:ut2\}; int\_seg(0; 3));
\\[0ex]locl(mkid\{choose1:ut2\});
\\[0ex]p{-}outcome(ternary{-}fps);
\\[0ex]mkid\{v1:ut2\};
\\[0ex](inl ($\lambda$$s$,$v$. $v$) )))))))
\-\-\-\-\-\-
\end{tabbing}